Nuprl Lemma : select_member
11,40
postcript
pdf
T
:Type,
L
:(
T
List),
i
:int_seg(0; ||
L
||). (
L
[
i
]
L
)
latex
Definitions
False
,
A
,
P
Q
,
prop{i:l}
,
A
B
,
t
T
,
A
c
B
,
,
x
:
A
.
B
(
x
)
,
(
x
l
)
,
x
:
A
.
B
(
x
)
,
P
Q
,
lelt(
i
;
j
;
k
)
,
int_seg(
i
;
j
)
Lemmas
int
seg
wf
,
length
wf1
,
select
wf
,
le
wf
origin
T:Type, L:(T List), i:int_seg(0; ||L||). (L[i] 
L) T:Type, L:(T List), i:int_seg(0; ||L||). (L[i] L) 
A
Q
B T
B
x:A. B(x) l)x:A. B(x) Q